onceR{$a:ut2, $done:ut2}
onceR(i)
== Rlist(cons(Rpre(i;
== Rlist(cons(Rpre(fpf-single(mkid{$done:ut2}; );
== Rlist(cons(Rpre(mkid{$a:ut2};
== Rlist(cons(Rpre(unit-fps;
== Rlist(cons(Rpre((s.es-state-ap(s; mkid{$done:ut2})));
== Rlist(cons(cons(Rinit(i; ; mkid{$done:ut2}; (inl ff ));
== Rlist(cons(cons(cons(Reffect(i;
== Rlist(cons(cons(cons(Reffect(fpf-single(mkid{$done:ut2}; );
== Rlist(cons(cons(cons(Reffect(locl(mkid{$a:ut2});
== Rlist(cons(cons(cons(Reffect(p-outcome(unit-fps);
== Rlist(cons(cons(cons(Reffect(mkid{$done:ut2};
== Rlist(cons(cons(cons(Reffect((inl (s,v. tt) ));
== Rlist(cons(cons(cons(cons(Rframe(i; ; mkid{$done:ut2}; cons(locl(mkid{$a:ut2}); [])); []))))
== Rlist() 

latex

Definitions

Rlist(L), Rpre(loc; ds; a; p; P), b, es-state-ap(s; x), Rinit(loc; T; x; v), ff, Reffect(loc; ds; knd; T; x; f), fpf-single(x; v), p-outcome(p), unit-fps, inl x , x.A(x), tt, Rframe(loc; T; x; L), , cons(car; cdr), locl(a), mkid{$x:ut2}, []